// Copyright (c) eBPF for Windows contributors
// SPDX-License-Identifier: MIT
// This work is derived from:
// https://github.com/project-everest/everparse/blob/2b53ee3fd4e0db6cd208c4cc65c13c5bd49c2863/src/3d/tests/ELF.3d

/*

  3d Specification of the 64-bit ELF format

  ELF resources: https://man7.org/linux/man-pages/man5/elf.5.html
                 https://github.com/torvalds/linux/blob/master/include/uapi/linux/elf.h
                 https://www.youtube.com/watch?v=nC1U1LJQL8o

  An ELF file consists of an ELF header, a program header table, and a section header table.

  Both the tables are optional.

  The ELF header starts at offset 0 in the file, and among other fields, contains the
  offsets of and the number of entries in the program header table and the section header table.

  These two tables then describe the rest of the file. Roughly:
              -------------------------------
             |                               |
             |                  -------------|------------------
             |                 |             |                  |
             |                 |            \ /                \ /
   ----------------------------------------------------------------------
  |..|ph_offset|ph_num|..|sh_offset|sh_num|..|ph table|file data|sh table|
   ----------------------------------------------------------------------

  |<---------------ELF Header--------------->|

  Where ph_table contains ph_num entries, sh_table contains sh_num entries,
  and both describe sections in the rest of the file (i.e., in the file data part).

  This specification validates the:
  - ELF header
  - Program Header table (that it contains ph_num entries,
                          and points to valid parts of the rest of the file).
  - Section Header table (that it contains sh_num entries,
                          and points to valid parts of the rest of the file).

  Though it is possible to do it in 3d, we do not validate individual sections/segments yet.

  See the ELF type at the end, that's the entrypoint for the specification.
*/


#define MAX_UINT32 0xffffffff

typedef UINT8 UCHAR;

typedef struct _ZeroByte
{
    UINT8 zero { zero == 0 };
} ZeroByte;

// Address type is either UINT64 or UINT32 depending on the architecture.
// For now, the spec supports only 64 bit arch, later we could parameterize
// the Address type.
// The same goes for the OFFSET type.

typedef UINT64 ADDRESS;

typedef UINT64 OFFSET;

//
// The first 4 bytes of the e_ident array in the ELF header.
//

#define ELFMAG0    0x7f
#define ELFMAG1    0x45  //'E'
#define ELFMAG2    0x4c  //'L'
#define ELFMAG3    0x46  //'F'

//
// The largest allowed value of the E_PHNUM field in the ELF Header.
//

#define PN_XNUM        0xffff

//
// The largest allowed value of the E_SHNUM field in the ELF Haeder.
//

#define SHN_LORESERVE  0xff00

//
// Value of E_SHSTRNDX when the ELF file has no Section Header table.
//

#define SHN_UNDEF      0

//
// Enums for ELF class, data, OS ABI.
// Used to type the fields in the ELF header.
//

UINT8 enum ELFCLASS
{
  ELFCLASSNONE = 0,
  ELFCLASS32,
  ELFCLASS64
}

UINT8 enum ELFDATA
{
  ELFDATANONE = 0,
  ELFDATA2LSB,
  ELFDATA2MSB
}

UINT8 enum ELFOSABI
{
  ELFOSABI_NONE = 0,
  ELFOSABI_SYSV,
  ELFOSABI_HPUX,
  ELFOSABI_NETBSD,
  ELFOSABI_LINUX,
  ELFOSABI_SOLARIS,
  ELFOSABI_IRIX,
  ELFOSABI_FREEBSD,
  ELFOSABI_TRU64,
  ELFOSABI_ARM,
  ELFOSABI_STANDALONE,
}

//
// Last 7 bytes of the ELF header are 0s.
//

#define E_IDENT_PADDING_SIZE    7


//
// The e_ident array in the ELF header.
//

typedef struct _E_IDENT
{
  //The first four bytes are 0x7f followed by 'E', 'L', and 'F'.

  UCHAR    ZERO    { ZERO == ELFMAG0 };
  UCHAR    ONE     { ONE == ELFMAG1 };
  UCHAR    TWO     { TWO == ELFMAG2 };
  UCHAR    THREE   { THREE == ELFMAG3 };

  ELFCLASS FOUR    { FOUR == ELFCLASS64 };  //This 3d spec applies to 64-bit only currently.

  ELFDATA  FIVE;

  UCHAR    SIX     { SIX == 1 };  //ELF specification version is always set to 1.

  ELFOSABI SEVEN;

  ZeroByte EIGHT;  //ABI version, always set to 0.

  ZeroByte NINE_FIFTEEN[E_IDENT_PADDING_SIZE];  //padding, remaining 7 bytes are 0.
} E_IDENT;

//
// The object file type
//

UINT16 enum ELF_TYPE
{
  ET_NONE = 0,
  ET_REL,
  ET_EXEC,
  ET_DYN,
  ET_CORE
}

/*

  A Program Header table entry.

  Arguments:

  * OFFSET ElfFileSize: Size of the ELF file.

  */

typedef struct _PROGRAM_HEADER_TABLE_ENTRY (OFFSET ElfFileSize)
{
  UINT32    P_TYPE;

  UINT32    P_FLAGS  { P_FLAGS <= 7 };

  OFFSET    P_OFFSET;

  ADDRESS   P_VADDR;

  ADDRESS   P_PADDR;

  //
  // Check that the pointed to segment lies within the file.
  //

  UINT64    P_FILESZ  { P_FILESZ < ElfFileSize &&
                        P_OFFSET <= ElfFileSize - P_FILESZ };
  UINT64    P_MEMSZ;

  UINT64    P_ALIGN;
} PROGRAM_HEADER_TABLE_ENTRY;


/*
  Type for (optional) Program Header table.

  Arguments:

  * UINT16 PhNum: number of Program Header table entries, from the ELF header.

  * OFFSET ElfFileSize: total size of the ELF file,
    to check that all entries describe parts of the file that are in valid range.

  */

casetype _PROGRAM_HEADER_TABLE_OPT (UINT16 PhNum,
				    OFFSET ElfFileSize)
{
  switch (PhNum)
  {
    case 0:
      unit    Empty;
    default:
      PROGRAM_HEADER_TABLE_ENTRY(ElfFileSize)    Tbl[:byte-size sizeof (PROGRAM_HEADER_TABLE_ENTRY) * PhNum]
   }
} PROGRAM_HEADER_TABLE_OPT;


//
//When a section is of type SH_NOBITS, its size is not really the size that it occupies.
//

#define SH_NOBITS        8

/*

  Type for the Section Header table entry.

  Arguments:

  * UINT16 ShNum: number of Section Header table entries.

  * OFFSET ElfFileSize: size of the ELF file.

  */

typedef struct _SECTION_HEADER_TABLE_ENTRY (UINT16 ShNum,
					    OFFSET ElfFileSize)
{
  UINT32        SH_NAME;

  UINT32        SH_TYPE;

  UINT64        SH_FLAGS;

  ADDRESS       SH_ADDR;

  OFFSET        SH_OFFSET;
  UINT64        SH_SIZE        { SH_TYPE == SH_NOBITS || (SH_SIZE <= ElfFileSize && SH_OFFSET <= ElfFileSize - SH_SIZE) };

  // It is another index in the Section Header Table.

  UINT32        SH_LINK        { SH_LINK < ShNum };

  UINT32        SH_INFO;

  UINT64        SH_ADDRALIGN;
  UINT64        SH_ENTSIZE;
} SECTION_HEADER_TABLE_ENTRY;


/*

  Type for the Section Header table, including the part of the ELF file
  between the Program Header table and the Section Header table.

  Arguments:

  * OFFSET PhTableEnd: the offset at which Program Header table ends.

  * UINT64 ShOff: offset of the Section Header table as in the ELF header.

  * UINT16 ShNum: number of Section Header table entries.

  * OFFSET ElfFileSize: size of the ELF file.

  */

typedef struct _SECTION_HEADER_TABLE (OFFSET PhTableEnd,
                                      UINT64 ShOff,
                                      UINT16 ShNum,
				      OFFSET ElfFileSize)
where (PhTableEnd <= ShOff && ShOff - PhTableEnd <= MAX_UINT32)
{
  UINT8        PHTABLE_SHTABLE_GAP[(UINT32) (ShOff - PhTableEnd)];

  SECTION_HEADER_TABLE_ENTRY(ShNum, ElfFileSize)    SHTABLE[:byte-size sizeof (SECTION_HEADER_TABLE_ENTRY) * ShNum];

  //
  // Check that we have consumed all the bytes in the file.
  //

  unit        EndOfFile
  {:on-success var x = field_pos; return (x == ElfFileSize); };
} SECTION_HEADER_TABLE;


/*

  An auxiliary type to just check that there are ElfFileSize - PhTableEnd
  bytes after the Program Header table, when there is no Section Header table.

  Arguments:

  * OFFSET PhTableEnd: the offset at which Program Header table ends.

  * UINT64 ElfFileSize: size of the ELF file.

  */

typedef struct _NO_SECTION_HEADER_TABLE (OFFSET PhTableEnd,
					 UINT64 ElfFileSize)
where (PhTableEnd <= ElfFileSize && ElfFileSize - PhTableEnd <= MAX_UINT32)
{
  UINT8        Rest[:byte-size (UINT32) (ElfFileSize - PhTableEnd)];
} NO_SECTION_HEADER_TABLE;


/*

  Type for the optional Section Header table.

  Arguments:

  * OFFSET PhTableEnd: The offset at which Program Header table ends.
    If there is no Program Header table in the file, this is the end of the ELF header.

  * OFFSET ShOff: The offset of the Section Header table as in the ELF header.

  * UINT16 ShNum: The number of Section Header table entries.

  * OFFSET ElfFileSize: The size of the ELF file.

  */

casetype _SECTION_HEADER_TABLE_OPT (OFFSET PhTableEnd,
                                    OFFSET ShOff,
                                    UINT16 ShNum,
				    OFFSET ElfFileSize)
{
  switch (ShNum)
  {
    //
    // When there is no Section Header table,
    // the following type ensures that there are at least ElfFileSize - PhTableEnd
    // bytes remaining in the file.
    //
    case 0:
      NO_SECTION_HEADER_TABLE(PhTableEnd, ElfFileSize)                   NoTbl;

    default:
      SECTION_HEADER_TABLE(PhTableEnd, ShOff, ShNum, ElfFileSize)        Tbl;
  }
} SECTION_HEADER_TABLE_OPT;

/*

  The main ELF type.

  Arguments:

  * UINT64 ElfFileSize: the size of the ELF file.
  */

entrypoint
typedef struct _ELF (UINT64 ElfFileSize)
{
  // ELF HEADER BEGIN

  E_IDENT          IDENT;
  ELF_TYPE         E_TYPE       { E_TYPE != ET_NONE };

  //
  // We can restrict the values of E_MACHINE by making its type an enum, for example.
  // The elf man page lists some possible values, but that list does not seem to be exhaustive.
  //

  UINT16           E_MACHINE;
  UINT32           E_VERSION    { E_VERSION == 1 };
  ADDRESS          E_ENTRY;

  OFFSET           E_PHOFF;  // See E_PHNUM below

  OFFSET           E_SHOFF;
  UINT32           E_FLAGS;

  //
  // The sizes of the ELF Header, and each Program Header entry and Section Header entry
  // are fixed statically, so we will restrict these values in the ELF header.
  //

  UINT16           E_EHSIZE     { E_EHSIZE == sizeof (this) };

  UINT16           E_PHENTSIZE;

  //
  // When the number of entries is more than PN_XNUM,
  // the ELF spec describes an alternate scheme for getting E_PHNUM,
  // our 3d spec does not implement that alternate scheme yet.
  //
  // Similarly for E_SHNUM
  //

  //
  // When the ELF file has no Program Header table,
  // E_PHNUM and E_PHOFF are 0
  // else, is it always the case that the table starts immediately after the ELF Header?
  //

  UINT16           E_PHNUM
    { (E_PHNUM == 0 && E_PHOFF == 0) ||  // No program Header table.
      (0 < E_PHNUM && E_PHNUM < PN_XNUM &&
       sizeof (this) == E_PHOFF &&  //Program Header table starts immediately after the ELF Header.
       E_PHENTSIZE == sizeof (PROGRAM_HEADER_TABLE_ENTRY)) };

  UINT16           E_SHENTSIZE;


  UINT16           E_SHNUM
    { (E_SHNUM == 0 && E_SHOFF == 0) ||  // No section Header table.
      (0 < E_SHNUM && E_SHNUM < SHN_LORESERVE &&
       E_SHENTSIZE == sizeof (SECTION_HEADER_TABLE_ENTRY)) };

  //
  // Either no Section Header table or a valid index into that table.
  //

  UINT16           E_SHSTRNDX
    { (E_SHNUM == 0 && E_SHSTRNDX == SHN_UNDEF) ||
      (0 < E_SHNUM  && E_SHSTRNDX < E_SHNUM) };

  // ELF HEADER END


  // (Optional) Program Header table.

  PROGRAM_HEADER_TABLE_OPT (E_PHNUM,
			    ElfFileSize)            PH_TABLE;

  // (Optional) Section Header Table.

  SECTION_HEADER_TABLE_OPT ((E_PHNUM == 0) ? E_EHSIZE : E_PHOFF + (sizeof (PROGRAM_HEADER_TABLE_ENTRY) * E_PHNUM),
                            E_SHOFF,
                            E_SHNUM,
			    ElfFileSize)            SH_TABLE;
} ELF;
